\begin{tabbing}
$\forall$\=$A$, $C$:Type, $B$:($A$$\rightarrow$Type), ${\it eqa}$:EqDecider($A$), ${\it eqc}$:EqDecider($C$), $r$:($A$$\rightarrow$$C$), $f$:$a$:$A$ fp$\rightarrow$ $B$($a$),\+
\\[0ex]$c$:$C$.
\-\\[0ex]($\uparrow$$c$ $\in$ dom(rename($r$;$f$))) $\Leftarrow\!\Rightarrow$ ($\exists$$a$:$A$. (($\uparrow$$a$ $\in$ dom($f$)) c$\wedge$ ($c$ = $r$($a$))))
\end{tabbing}